es:ES, ff:FIFO, p:(E), e:E, sndr, rcvr:ff.C.
(e:E. Dec(p(e)))
 (e:E. Dec(ff.S(rcvr,sndr,e)))
 (e:E. Dec(ff.R(sndr,e)))
 Dec([e: sndr p rcvr]) 

latex

Definitions	A, A c B, {T}, P  Q, Dec(P), x:A. B(x), P & Q, [e: i p j], t  T, x(s), P  Q, , x:A. B(x), False
Lemmas	fifoSender wf, decidable cand, event system wf, FIFO wf, fifoC wf, fifoS wf, fifoR wf, decidable wf, es-E wf